\begin{tabbing}
Feasible($M$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$$\in$dom(1of($M$)). $T$=1of($M$)($x$) $\Rightarrow$  $T$\+
\\[0ex]\& $\forall$$k$$\in$dom(1of(2of($M$))). $T$=1of(2of($M$))($k$) $\Rightarrow$  Dec($T$)
\\[0ex]\& \=$\forall$$a$$\in$dom(1of(2of(2of(2of($M$))))). \+
\\[0ex]
\\[0ex]$p$\==1of(2of(2of(2of($M$))))($a$) $\Rightarrow$ \+
\\[0ex]$\forall$$s$:State(1of($M$)). Dec($\exists$$v$:1of(2of($M$))(locl($a$))?Top. $p$($s$,$v$))
\-\-\\[0ex]\& $\forall$$x$$\in$dom(1of($M$)). $T$=1of($M$)($x$) $\Rightarrow$  AtomFree(Type;$T$)
\\[0ex]\& $\forall$$k$$\in$dom(1of(2of($M$))). $T$=1of(2of($M$))($k$) $\Rightarrow$  AtomFree(Type;$T$)
\\[0ex]\& ma{-}frame{-}compat($M$;$M$)
\-
\end{tabbing}